(declare-const fpv2 Float32)
(declare-const fpv3 Float32)
(declare-const fpv5 Float32)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const r1 Real)
(declare-const r3 Real)
(declare-const r4 Real)
(declare-const r5 Real)
(declare-const r9 Real)
(declare-const r10 Real)
(push)
(declare-const r11 Real)
(declare-const r12 Real)
(declare-const v3 Bool)
(declare-const fpv13 Float32)
(assert (not (>= r4 r11 241.63444 r12)))
(assert (xor v2 v1 v1 (>= 2993.0 r4 628948.0) v0))
(push)
(assert (or (fp.leq ((_ to_fp 8 24) RNA 0.136742) (fp.div RNA fpv13 ((_ to_fp 8 24) RNE 587212.0)) ((_ to_fp 8 24) RTN 368768.0) fpv5 ((_ to_fp 8 24) RTZ 4.308358)) (=> v1 (= r10 2003667863.0 r9)) (not v1) (fp.eq ((_ to_fp 8 24) RNA 0.136742) ((_ to_fp 8 24) RTN 368768.0)) (>= r4 r11 241.63444 r12) v3 v1 (not (>= r4 r11 241.63444 r12)) v0 v0))
(check-sat)
